proof(L1): close ADMIT 2 — remove false region_liveness lemma (4→3 admits) + v2 proof audit#322
Merged
Conversation
… the honest val_region_no_exit reformulation The provably-false region_liveness_at_split_l1_gen (asserting In rv R -> In rv R' unconditionally; false in the T_Region_Active_L1 r = rv sub-case, witness ERegion rv (EI32 5) at R = [rv]) is removed. Its 13 consumers in subst_typing_gen_l1_m now route region liveness through the TRUE, Qed region_liveness_no_exit_l1_gen, supplied with a new honest premise val_region_no_exit threaded through the substitution chain (subst_typing_gen_l1_m / subst_typing_gen_l1 / subst_preserves_typing_l1) and the L2 beta-case lemmas (preservation_l2_app_eff_beta_linear / _l1). Verified by rebuilt coqc 8.18.0 + Print Assumptions: - formal/ outer Admitted: 4 -> 3. region_liveness removed; only the sacrosanct legacy Semantics.v preservation, step_pop, and the preservation_l1 capstone remain. - The substitution chain and both L2 beta-case lemmas flip from "depends on a false axiom" to "Closed under the global context" (axiom-free, carrying the honest premise instead). - preservation_l3 stays unconditionally axiom-free. This is the sanctioned honest closure recorded in Semantics_L1.v's 2026-06-16 call-site audit and PROOF-NEEDS.md, not ad-hoc patching of the legacy judgment. Also corrects the PROOF-NEEDS.md §4 status-gate marker to ground truth (was 5, now 3; scripts/status-gate.sh --proofs passes) and reconciles the per-file table + the in-source audit comments. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL
hyperpolymath
marked this pull request as ready for review
June 26, 2026 21:13
hyperpolymath
added a commit
that referenced
this pull request
Jun 27, 2026
…SPDX + trusted-base) (#329) ## Summary Two governance checks have been red on **every** PR (#322–#324) for reasons unrelated to any diff — both are repo-level. This clears the two that are in ephapax's control. Fixes were derived from the **exact `standards@d135b05` check-script regexes** (fetched via raw HTTPS and verified locally, not guessed). ### 1. `governance / Licence consistency` Root `LICENSE` is the verbatim MPL-2.0 text with **no SPDX header**. `check-licence-consistency.sh` does: ```sh grep -m1 -E '^[[:space:]]*SPDX-License-Identifier:' "$lic_file" ``` then normalises the identifier and checks it matches the manifest. **Fix:** prepend `SPDX-License-Identifier: MPL-2.0` (normalises to `mpl-2.0`, matches `Cargo.toml` `license = "MPL-2.0"`). Verified the grep now matches. ### 2. `governance / Trusted-base reduction policy` `check-trusted-base.sh` flags `^[[:space:]]*(Axiom|Admitted|admit\.)`. `formal/RegionEnvL1.v:17` is a **prose comment** — *"Axiom budget: this file is axiom-free"* — that happens to start with "Axiom". A false positive. **Fix:** reword to *"On the axiom budget: …"* so the line no longer matches (verified). Chosen over a `.trusted-base-ignore` entry deliberately: the file stays **fully scanned**, so a genuine future axiom there is still caught — and a `TRUSTED:`/`AXIOM:` inline annotation would be *false* (the file really is axiom-free; that's the whole point of `RegionEnvL1.v`). ## Not fixable here `scan / Hypatia Neurosymbolic Analysis` fails on an Elixir `CompileError` (`real_subdirs`) **inside the `standards`/Hypatia repo** — out of ephapax's reach. Flagging, not fixing. ## Verification - Both fixes checked against the actual fetched regexes (`standards@d135b05`). - `formal/RegionEnvL1.v` still compiles under `coqc 8.18.0` (comment-only change). - 2 files, +3/−1. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL --- _Generated by [Claude Code](https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL)_ Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
A ground-truth audit of every v2 proof in the repo (rebuilt
coqc 8.18.0,Print Assumptionson every keystone — not doc-trust), plus one real closure: the provably-falseregion_liveness_at_split_l1_genlemma is removed and its consumers re-routed through the true graded lemma. OuterAdmitted.count: 4 → 3.Everything here is mechanically verified — only proofs that actually compile + pass
Print Assumptionsare claimed.What ran (provers installed in-session)
formal/*.vcompile (exit 0);Print Assumptionsauditedwasm_e2eall pass (with the optionaltyped-wasm-verifygit dep — itself 403-blocked — disabled; not part of this diff)The closure (the substantive change)
region_liveness_at_split_l1_genassertedIn rv R -> In rv R'unconditionally, which is false in theT_Region_Active_L1r = rvsub-case (witnessERegion rv (EI32 5)atR = [rv]). It satAdmittedand was consumed at 13 sites insubst_typing_gen_l1_m.This PR realises the honest closure the source's own 2026-06-16 call-site audit prescribed:
val_region_no_exit v epremise tosubst_typing_gen_l1_m, threaded throughsubst_typing_gen_l1/subst_preserves_typing_l1and the L2 β-case lemmaspreservation_l2_app_eff_beta_linear/_l1.Qedregion_liveness_no_exit_l1_gen(proved fromcnt-monotonicity).Counterexample_RegionShrink.v.Verified outcome (
Print Assumptions)formal/outerAdmitted.: 4 → 3 — only the sacrosanct legacySemantics.v preservation,step_pop_disjoint_from_type_l1, and thepreservation_l1capstone remain.preservation_l3stays unconditionally axiom-free.scripts/status-gate.sh --proofspasses (the marker was stale at5; corrected to ground-truth3).Files
formal/Semantics_L1.v— premise + 13-site rethread; false lemma removed; audit comments updated.formal/TypingL2.v— premise threaded through the two β-case lemmas.PROOF-NEEDS.md— §4 marker5 → 3, per-file table + parenthetical reconciled tocoqcground truth.Scope / fences
This is the sanctioned per-layer reformulation (PROOF-NEEDS.md §5.4 / the in-source ADMIT-2 audit), not patching the legacy judgment. The remaining
step_pop(eliminator-fork research) andpreservation_l1(capstone, gated onstep_pop) are left fenced, with the residual region-liveness-through-reduction obligation now sitting explicitly as theval_region_no_exitpremisepreservation_l1will owe.🤖 Generated with Claude Code
https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL
Generated by Claude Code